Nuprl Lemma : gcd_reduce_property
11,40
postcript
pdf
p
,
q
:
.
spreadn(gcd_reduce(
p
;
q
);
spreadn(
g
,
a
,
b
.((
p
= (
a
*
g
))
(
q
= (
b
*
g
))
coprime(
a
;
b
)
((
p
*
b
) = (
a
*
q
))))
latex
Definitions
guard(
T
)
,
sq_type(
T
)
,
prop{i:l}
,
P
Q
,
x
:
A
.
B
(
x
)
,
t
T
,
spreadn(
a
;
w
,
x
,
y
,
z
.
t
(
w
;
x
;
y
;
z
))
,
P
Q
,
gcd_reduce(
p
;
q
)
,
spreadn(
a
;
x
,
y
,
z
.
t
(
x
;
y
;
z
))
,
x
:
A
.
B
(
x
)
,
P
Q
,
P
Q
,
Lemmas
coprime
bezout
id
,
nat
wf
origin
p,q:
.
(q = (b * g)) coprime(a; b) ((p * b) = (a * q)))) p,q:.
(q = (b * g)) coprime(a; b) ((p * b) = (a * q)))) 
Q
x:A. B(x)
T Qx:A. B(x)
Q Q